Nuprl Definition : w-after
11,40
postcript
pdf
(
x
after
e
)(
t
) == s(
e
.1;(
e
.2)+1).
x
(
t
- 1)
latex
clarification:
w-after(
w
;
x
;
e
)(
t
) == w-s(
w
; (
e
.1); ((
e
.2)+1);
x
)(
t
- 1)
latex
Definitions
x
.
A
(
x
)
,
f
(
a
)
,
s(
i
;
t
).
x
,
t
.1
,
n
+
m
,
t
.2
,
r
-
s
,
#$n
FDL editor aliases
w-after
origin
x.A(x)x.A(x)